Issue2067b.agda:21,7-8
Nat !=< M₁.Mm.A n
when checking that the expression n has type M₁.Mm.A n
